$\forall$$w$:world\{i:l\}.
\\[0ex]($\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk. ($\uparrow$isrcv($l$;a($i$;$t$))) $\Rightarrow$ (destination($l$) = $i$))
\\[0ex]$\Rightarrow$ (w{-}machine{-}constraint($w$) $\in$ $\mathbb{P}$\{i'\})